Nuprl Definition : es-interface-filter
11,40
postcript
pdf
X
|
a
.
P
(
a
)(
e
) == case
X
(
e
) of inl(
a
) => if
P
(
a
) then inl
a
else inr
fi | inr(
b
) => inr
b
latex
Definitions
x
.
A
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
f
(
a
)
,
if
b
then
t
else
f
fi
,
inl
x
,
,
inr
x
FDL editor aliases
es-interface-filter
origin
fi | inr(b) => inr b fi | inr(b) => inr b 
x.A(x)